T:Type, as,bs:(T List), b:T. (as = append(as; cons(b; bs)))  False 

latex

Definitions	t  T, False, x:A. B(x), prop{i:l}, P  Q, P  Q, P  Q, P  Q, append(as; bs), top, subtype(S; T), ||as||, A, P  Q, decidable(P)
Lemmas	decidable false, append-cancellation, length wf1, append nil sq, top wf, append wf, false wf